pre{-}init{-}p(${\it es}$;$i$;${\it ds}$;${\it init}$;$T$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\exists$$v$:$T$. $P$(($\lambda$$x$.fpf{-}cap(${\it init}$;IdDeq;$x$;$\cdot$)),$v$)) $\Rightarrow$ ($\exists$$e$:es{-}E(${\it es}$). es{-}loc(${\it es}$; $e$) $=$ $i$ $\in$ Id)